Termination w.r.t. Q proof of /tmp/tmpWHGmti/08.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

E1(h1(w), h2(w), x, y, z, w) → E2(x, x, y, z, z, w)
F1(x, a) → G2(x, x)
E2(f1(w, w), x, y, z, f2(w, w), w) → E3(x, y, x, y, y, z, y, z, x, y, z, w)
F2(x, a) → G2(x, x)
G2(a, x) → H1(x)
E1(x1, x1, x, y, z, a) → E5(x1, x, y, z)
F1(a, x) → G1(x, x)
E4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → E1(x1, x1, x, y, z, w)
G1(x, a) → H2(x)
F2(a, x) → G1(x, x)
E4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → E5(x1, x, y, z)
G1(a, x) → H1(x)
G2(x, a) → H2(x)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)

The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

E1(h1(w), h2(w), x, y, z, w) → E2(x, x, y, z, z, w)
F1(x, a) → G2(x, x)
E2(f1(w, w), x, y, z, f2(w, w), w) → E3(x, y, x, y, y, z, y, z, x, y, z, w)
F2(x, a) → G2(x, x)
G2(a, x) → H1(x)
E1(x1, x1, x, y, z, a) → E5(x1, x, y, z)
F1(a, x) → G1(x, x)
E4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → E1(x1, x1, x, y, z, w)
G1(x, a) → H2(x)
F2(a, x) → G1(x, x)
E4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → E5(x1, x, y, z)
G1(a, x) → H1(x)
G2(x, a) → H2(x)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)

The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 10 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

E1(h1(w), h2(w), x, y, z, w) → E2(x, x, y, z, z, w)
E4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → E1(x1, x1, x, y, z, w)
E2(f1(w, w), x, y, z, f2(w, w), w) → E3(x, y, x, y, y, z, y, z, x, y, z, w)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)

The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule E1(h1(w), h2(w), x, y, z, w) → E2(x, x, y, z, z, w) we obtained the following new rules:

E1(h1(x0), h2(x0), f1(y_0, y_1), x2, f2(y_5, y_6), x0) → E2(f1(y_0, y_1), f1(y_0, y_1), x2, f2(y_5, y_6), f2(y_5, y_6), x0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

E1(h1(x0), h2(x0), f1(y_0, y_1), x2, f2(y_5, y_6), x0) → E2(f1(y_0, y_1), f1(y_0, y_1), x2, f2(y_5, y_6), f2(y_5, y_6), x0)
E4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → E1(x1, x1, x, y, z, w)
E2(f1(w, w), x, y, z, f2(w, w), w) → E3(x, y, x, y, y, z, y, z, x, y, z, w)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)

The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule E4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → E1(x1, x1, x, y, z, w) we obtained the following new rules:

E4(g1(x0, x0), x1, g2(x0, x0), x1, g1(x0, x0), x1, g2(x0, x0), x1, f1(y_4, y_5), x3, f2(y_7, y_8), x0) → E1(x1, x1, f1(y_4, y_5), x3, f2(y_7, y_8), x0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

E1(h1(x0), h2(x0), f1(y_0, y_1), x2, f2(y_5, y_6), x0) → E2(f1(y_0, y_1), f1(y_0, y_1), x2, f2(y_5, y_6), f2(y_5, y_6), x0)
E4(g1(x0, x0), x1, g2(x0, x0), x1, g1(x0, x0), x1, g2(x0, x0), x1, f1(y_4, y_5), x3, f2(y_7, y_8), x0) → E1(x1, x1, f1(y_4, y_5), x3, f2(y_7, y_8), x0)
E2(f1(w, w), x, y, z, f2(w, w), w) → E3(x, y, x, y, y, z, y, z, x, y, z, w)
E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)

The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule E3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → E4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) we obtained the following new rules:

E3(x0, x0, x1, x1, x2, x2, x3, x3, f1(y_16, y_17), x5, f2(y_19, y_20), x7) → E4(x0, x0, x1, x1, x2, x2, x3, x3, f1(y_16, y_17), x5, f2(y_19, y_20), x7)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

                    ↳ QDP

                      ↳ ForwardInstantiation

Q DP problem:
The TRS P consists of the following rules:

E3(x0, x0, x1, x1, x2, x2, x3, x3, f1(y_16, y_17), x5, f2(y_19, y_20), x7) → E4(x0, x0, x1, x1, x2, x2, x3, x3, f1(y_16, y_17), x5, f2(y_19, y_20), x7)
E1(h1(x0), h2(x0), f1(y_0, y_1), x2, f2(y_5, y_6), x0) → E2(f1(y_0, y_1), f1(y_0, y_1), x2, f2(y_5, y_6), f2(y_5, y_6), x0)
E2(f1(w, w), x, y, z, f2(w, w), w) → E3(x, y, x, y, y, z, y, z, x, y, z, w)
E4(g1(x0, x0), x1, g2(x0, x0), x1, g1(x0, x0), x1, g2(x0, x0), x1, f1(y_4, y_5), x3, f2(y_7, y_8), x0) → E1(x1, x1, f1(y_4, y_5), x3, f2(y_7, y_8), x0)

The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule E2(f1(w, w), x, y, z, f2(w, w), w) → E3(x, y, x, y, y, z, y, z, x, y, z, w) we obtained the following new rules:

E2(f1(x0, x0), f1(y_8, y_9), x2, f2(y_11, y_12), f2(x0, x0), x0) → E3(f1(y_8, y_9), x2, f1(y_8, y_9), x2, x2, f2(y_11, y_12), x2, f2(y_11, y_12), f1(y_8, y_9), x2, f2(y_11, y_12), x0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

                    ↳ QDP

                      ↳ ForwardInstantiation

                        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

E3(x0, x0, x1, x1, x2, x2, x3, x3, f1(y_16, y_17), x5, f2(y_19, y_20), x7) → E4(x0, x0, x1, x1, x2, x2, x3, x3, f1(y_16, y_17), x5, f2(y_19, y_20), x7)
E1(h1(x0), h2(x0), f1(y_0, y_1), x2, f2(y_5, y_6), x0) → E2(f1(y_0, y_1), f1(y_0, y_1), x2, f2(y_5, y_6), f2(y_5, y_6), x0)
E2(f1(x0, x0), f1(y_8, y_9), x2, f2(y_11, y_12), f2(x0, x0), x0) → E3(f1(y_8, y_9), x2, f1(y_8, y_9), x2, x2, f2(y_11, y_12), x2, f2(y_11, y_12), f1(y_8, y_9), x2, f2(y_11, y_12), x0)
E4(g1(x0, x0), x1, g2(x0, x0), x1, g1(x0, x0), x1, g2(x0, x0), x1, f1(y_4, y_5), x3, f2(y_7, y_8), x0) → E1(x1, x1, f1(y_4, y_5), x3, f2(y_7, y_8), x0)

The TRS R consists of the following rules:

f1(a, x) → g1(x, x)
f1(x, a) → g2(x, x)
f2(a, x) → g1(x, x)
f2(x, a) → g2(x, x)
g1(a, x) → h1(x)
g1(x, a) → h2(x)
g2(a, x) → h1(x)
g2(x, a) → h2(x)
h1(a) → i
h2(a) → i
e1(h1(w), h2(w), x, y, z, w) → e2(x, x, y, z, z, w)
e1(x1, x1, x, y, z, a) → e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w) → e3(x, y, x, y, y, z, y, z, x, y, z, w)
e2(x, x, y, z, z, a) → e6(x, y, z)
e2(i, x, y, z, i, a) → e6(x, y, z)
e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a) → e6(x, y, z)
e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a) → e5(x1, x, y, z)
e4(x, x, x, x, x, x, x, x, x, x, x, a) → e6(x, x, x)
e5(i, x, y, z) → e6(x, y, z)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.